1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  -/
  6  
  7  import analysis.normed_space.operator_norm linear_algebra.finite_dimensional tactic.omega
src         └─────────────────────────────────┘ └───────────────────────────────┘ └──────────┘
  8  
  9  /-!
 10  # Finite dimensional normed spaces over complete fields
 11  
 12  Over a complete nondiscrete field, in finite dimension, all norms are equivalent and all linear maps
 13  are continuous. Moreover, a finite-dimensional subspace is always complete and closed.
 14  
 15  ## Main results:
 16  
 17  * `linear_map.continuous_of_finite_dimensional` : a linear map on a finite-dimensional space over a
 18    complete field is continuous.
 19  * `finite_dimensional.complete` : a finite-dimensional space over a complete field is complete. This
 20    is not registered as an instance, as the field would be an unknown metavariable in typeclass
 21    resolution.
 22  * `submodule.closed_of_finite_dimensional` : a finite-dimensional subspace over a complete field is
 23    closed
 24  * `finite_dimensional.proper` : a finite-dimensional space over a proper field is proper. This
 25    is not registered as an instance, as the field would be an unknown metavariable in typeclass
 26    resolution. It is however registered as an instance for `𝕜 = ℝ` and `𝕜 = ℂ`. As properness
 27    implies completeness, there is no need to also register `finite_dimensional.complete` on `ℝ` or
 28    `ℂ`.
 29  
 30  ## Implementation notes
 31  
 32  The fact that all norms are equivalent is not written explicitly, as it would mean having two norms
 33  on a single space, which is not the way type classes work. However, if one has a
 34  finite-dimensional vector space `E` with a norm, and a copy `E'` of this type with another norm,
 35  then the identities from `E` to `E'` and from `E'`to `E` are continuous thanks to
 36  `linear_map.continuous_of_finite_dimensional`. This gives the desired norm equivalence.
 37  -/
 38  
 39  universes u v w x
 40  
 41  open set finite_dimensional
 42  open_locale classical
 43  
 44  -- To get a reasonable compile time for `continuous_equiv_fun_basis`, typeclass inference needs
 45  -- to be guided.
 46  local attribute [instance, priority 10000] pi.module normed_space.to_module
id                                              └───────┘ └────────────────────┘
src                                             └───────┘ └────────────────────┘
typ                                             └───────┘ └────────────────────┘
 47    submodule.add_comm_group submodule.module
id     └──────────────────────┘ └──────────────┘
src    └──────────────────────┘ └──────────────┘
typ    └──────────────────────┘ └──────────────┘
 48    linear_map.finite_dimensional_range Pi.complete nondiscrete_normed_field.to_normed_field
id     └─────────────────────────────────┘ └─────────┘ └──────────────────────────────────────┘
src    └─────────────────────────────────┘ └─────────┘ └──────────────────────────────────────┘
typ    └─────────────────────────────────┘ └─────────┘ └──────────────────────────────────────┘
doc    └─────────────────────────────────┘
 49  
 50  set_option class.instance_max_depth 100
doc             └──────────────────────┘
 51  
 52  /-- A linear map on `ι → 𝕜` (where `ι` is a fintype) is continuous -/
 53  lemma linear_map.continuous_on_pi {ι : Type w} [fintype ι] {𝕜 : Type u} [normed_field 𝕜]
id                                                   └─────┘                 └──────────┘ 
src                                                  └─────┘                  └──────────┘
typ                                                  └─────┘                 └──────────┘ 
doc                                                  └─────┘                  └──────────┘
 54    {E : Type v}  [add_comm_group E] [vector_space 𝕜 E] [topological_space E]
id                    └────────────┘    └──────────┘     └───────────────┘ 
src                   └────────────┘     └──────────┘       └───────────────┘
typ                   └────────────┘    └──────────┘     └───────────────┘ 
doc                                      └──────────┘       └───────────────┘
 55    [topological_add_group E] [topological_vector_space 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) : continuous f :=
id      └───────────────────┘    └──────────────────────┘              └─┘     └────────┘ 
src     └───────────────────┘     └──────────────────────┘                   └─┘       └────────┘
typ     └───────────────────┘    └──────────────────────┘              └─┘     └────────┘ 
doc     └───────────────────┘     └──────────────────────┘                              └────────┘
 56  begin
st   └─────
 57    -- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
 58    -- function.
st   ───────────────
 59    have : (f : (ι → 𝕜) → E) =
id                            
src    └─────┘  └─┘    └┘  └┘
typ    └─────┘  └─┘   └┘ └┘
doc    └─────┘  └─┘    └┘  └┘ 
txt    └─────┘  └─┘    └┘  └┘ 
par    └─────┘  └─┘    └┘  └┘ 
pid    └───┘└┘  └─┘    └┘  └┘ 
st   ─────────────────────────────
 60           (λx, finset.sum finset.univ (λi:ι, x i • (f (λj, if i = j then 1 else 0)))),
id                 └────────┘ └─────────┘             
src  ────────┘  └─┘└────────┘└─────────┘  └┘ └┘      └─┘  └─┘  └────────────────┘
typ  ────────┘  └─┘└────────┘└─────────┘  └┘└┘     └─┘  └─┘  └────────────────┘
doc  ────────┘  └─┘          └─────────┘  └┘ └┘       └─┘  └─┘  └────────────────┘
txt  ────────┘  └─┘                       └┘ └┘       └─┘  └─┘  └────────────────┘
par  ────────┘  └─┘                       └┘ └┘       └─┘  └─┘  └────────────────┘
pid  ────────┘  └─┘                       └┘ └┘       └─┘  └─┘  └────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────┘
 61      by { ext x, exact f.pi_apply_eq_sum_univ x },
id                         └────────────────────┘ 
src           └───┘  └────┘└────────────────────┘ 
typ           └───┘  └────┘└────────────────────┘
doc           └───┘  └────┘└────────────────────┘ 
txt           └───┘  └────┘                       
par           └───┘  └────┘                       
pid              └┘                              
st          └────┘└───────────────────────────────┘└┘
 62    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
 63    refine continuous_finset_sum _ (λi hi, _),
id            └───────────────────┘
src    └─────┘└───────────────────┘└─┘  └──────┘
typ    └─────┘└───────────────────┘└─┘  └──────┘
doc    └─────┘                     └─┘  └──────┘
txt    └─────┘                     └─┘  └──────┘
par    └─────┘                     └─┘  └──────┘
pid                               └─┘  └──────┘
st   ──────────────────────────────────────────┘└─
 64    exact (continuous_apply i).smul continuous_const
id            └──────────────┘        └──────────────┘
src    └────┘ └──────────────┘ └─────┘└──────────────┘
typ    └────┘ └──────────────┘└─────┘└──────────────┘
doc    └────┘                  └─────┘                
txt    └────┘                  └─────┘                
par    └────┘                  └─────┘                
pid                           └─────┘                
st   ──────────────────────────────────────────────────┘
 65  end
st   └─┘
 66  
 67  section complete_field
 68  
 69  variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
id                           └──────────────────────┘
src                          └──────────────────────┘
typ                          └──────────────────────┘
doc                          └──────────────────────┘
 70  {E : Type v} [normed_group E] [normed_space 𝕜 E]
id                 └──────────┘     └──────────┘
src                └──────────┘     └──────────┘
typ                └──────────┘     └──────────┘
doc                └──────────┘     └──────────┘
 71  {F : Type w} [normed_group F] [normed_space 𝕜 F]
id                 └──────────┘     └──────────┘
src                └──────────┘     └──────────┘
typ                └──────────┘     └──────────┘
doc                └──────────┘     └──────────┘
 72  {F' : Type x} [add_comm_group F'] [vector_space 𝕜 F'] [topological_space F']
id                  └────────────┘      └──────────┘        └───────────────┘
src                 └────────────┘      └──────────┘        └───────────────┘
typ                 └────────────┘      └──────────┘        └───────────────┘
doc                                     └──────────┘        └───────────────┘
 73  [topological_add_group F'] [topological_vector_space 𝕜 F']
id    └───────────────────┘      └──────────────────────┘
src   └───────────────────┘      └──────────────────────┘
typ   └───────────────────┘      └──────────────────────┘
doc   └───────────────────┘      └──────────────────────┘
 74  [complete_space 𝕜]
id    └────────────┘
src   └────────────┘
typ   └────────────┘
doc   └────────────┘
 75  
 76  set_option class.instance_max_depth 150
doc             └──────────────────────┘
 77  
 78  /-- In finite dimension over a complete field, the canonical identification (in terms of a basis)
 79  with `𝕜^n` together with its sup norm is continuous. This is the nontrivial part in the fact that
 80  all norms are equivalent in finite dimension.
 81  Do not use this statement as its formulation is awkward (in terms of the dimension `n`, as the proof
 82  is done by induction over `n`) and it is superceded by the fact that every linear map on a
 83  finite-dimensional space is continuous, in `linear_map.continuous_of_finite_dimensional`. -/
 84  lemma continuous_equiv_fun_basis {n : ℕ} {ι : Type v} [fintype ι] (ξ : ι → E)
id                                                         └─────┘           
src                                                        └─────┘
typ                                                        └─────┘           
doc                                                         └─────┘
 85    (hn : fintype.card ι = n) (hξ : is_basis 𝕜 ξ) : continuous (equiv_fun_basis hξ) :=
id           └──────────┘           └──────┘      └────────┘  └─────────────┘ └┘
src          └──────────┘             └──────┘        └────────┘  └─────────────┘
typ          └──────────┘           └──────┘      └────────┘  └─────────────┘ └┘
doc          └──────────┘              └──────┘        └────────┘  └─────────────┘
 86  begin
 87    unfreezeI,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
 88    induction n with n IH generalizing ι E,
src    └────────┘ └─────────────────────────┘
typ    └────────┘ └─────────────────────────┘
doc    └────────┘ └─────────────────────────┘
txt    └────────┘ └─────────────────────────┘
par    └────────┘ └─────────────────────────┘
pid              └───────┘└───────────────┘
 89    { apply linear_map.continuous_of_bound _ 0 (λx, _),
src      └────┘                              └───┘  └───┘
typ      └────┘                              └───┘  └───┘
doc      └────┘                              └───┘  └───┘
txt      └────┘                              └───┘  └───┘
par      └────┘                              └───┘  └───┘
pid                                         └───┘  └───┘
 90      have : equiv_fun_basis hξ x = 0,
src      └─────┘                   └┘
typ      └─────┘                   └┘
doc      └─────┘                   └┘
txt      └─────┘                   └┘
par      └─────┘                   └┘
pid      └───┘└┘                   
 91        by { ext i, exact (fintype.card_eq_zero_iff.1 hn i).elim },
id                            └──────────────────────┘   └┘ 
src             └───┘  └────┘ └──────────────────────┘└─┘   └─────┘
typ             └───┘  └────┘ └──────────────────────┘└─┘└┘└─────┘
doc             └───┘  └────┘                         └─┘   └─────┘
txt             └───┘  └────┘                         └─┘   └─────┘
par             └───┘  └────┘                         └─┘   └─────┘
pid                └┘                                └─┘   └───┘└┘
st                         └───────────────────────────────────────┘└┘
 92      change ∥equiv_fun_basis hξ x∥ ≤ 0 * ∥x∥,
id              └─────────────┘ └┘        
src      └─────┘└─────────────┘   └─┘
typ      └─────┘└─────────────┘└┘ └─┘ 
doc      └─────┘ └─────────────┘     └─┘ 
txt      └─────┘                     └─┘ 
par      └─────┘                     └─┘ 
pid                                 └─┘ 
st   ──────────────────────────────────────────┘└─
 93      rw this,
id          └──┘
src      └─┘
typ      └─┘└──┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────┘└─
 94      simp [norm_nonneg] },
id             └─────────┘
src      └────┘└─────────┘└┘
typ      └────┘└─────────┘└┘
doc      └────┘           └┘
txt      └────┘           └┘
par      └────┘           └┘
pid                     
st   ──────────────────────┘└┘
 95    { haveI : finite_dimensional 𝕜 E := of_finite_basis hξ,
id               └────────────────┘      └─────────────┘ └┘
src      └──────┘└────────────────┘  └──┘└─────────────┘
typ      └──────┘└────────────────┘└──┘└─────────────┘└┘
doc      └──────┘└────────────────┘  └──┘└─────────────┘
txt      └──────┘                    └──┘               
par      └──────┘                    └──┘               
pid           └┘                    └──┘               
st   ───────────────────────────────────────────────────────┘└─
 96      -- first step: thanks to the inductive assumption, any n-dimensional subspace is equivalent
st   ────────────────────────────────────────────────────────────────────────────────────────────────
 97      -- to a standard space of dimension n, hence it is complete and therefore closed.
st   ──────────────────────────────────────────────────────────────────────────────────────
 98      have H₁ : ∀s : submodule 𝕜 E, findim 𝕜 s = n → is_closed (s : set E),
id                      └───────┘      └────┘        └───────┘      └─┘ 
src      └────────┘ └──┘└───────┘   └────┘     └───────┘  └─┘└─┘ 
typ      └────────┘ └──┘└───────┘   └────┘  └───────┘  └─┘└─┘
doc      └────────┘ └──┘└───────┘   └────┘     └───────┘  └─┘    
txt      └────────┘ └──┘                                  └─┘    
par      └────────┘ └──┘                                  └─┘    
pid      └─────┘└─┘ └──┘                                  └─┘    
st   ───────────────────────────────────────────────────────────────────────┘└─
 99      { assume s s_dim,
src        └────────────┘
typ        └────────────┘
doc        └────────────┘
txt        └────────────┘
par        └────────────┘
pid        └────────────┘
st   ─────┘└────────────┘└─
100        rcases exists_is_basis_finite 𝕜 s with ⟨b, b_basis, b_finite⟩,
id                └────────────────────┘  
src        └─────┘└────────────────────┘  └──────────────────────────┘
typ        └─────┘└────────────────────┘└──────────────────────────┘
doc        └─────┘                        └──────────────────────────┘
txt        └─────┘                        └──────────────────────────┘
par        └─────┘                        └──────────────────────────┘
pid                                      └──────────────────────────┘
st   ──────────────────────────────────────────────────────────────────┘└─
101        letI : fintype b := finite.fintype b_finite,
id                └─────┘     └────────────┘ └──────┘
src        └─────┘└─────┘ └──┘└────────────┘
typ        └─────┘└─────┘└──┘└────────────┘└──────┘
doc        └─────┘└─────┘ └──┘└────────────┘
txt        └─────┘        └──┘              
par        └─────┘        └──┘              
pid            └┘        └──┘              
st   ────────────────────────────────────────────────┘└─
102        have U : uniform_embedding (equiv_fun_basis b_basis).symm,
id                  └───────────────┘  └─────────────┘ └─────┘
src        └───────┘└───────────────┘ └─────────────┘       └────┘
typ        └───────┘└───────────────┘ └─────────────┘└─────┘└────┘
doc        └───────┘                  └─────────────┘       └────┘
txt        └───────┘                                        └────┘
par        └───────┘                                        └────┘
pid        └────┘└─┘                                        └───┘
st   ──────────────────────────────────────────────────────────────┘└─
103        { have : fintype.card b = n,
id                  └──────────┘    
src          └─────┘└──────────┘  
typ          └─────┘└──────────┘ 
doc          └─────┘└──────────┘  
txt          └─────┘              
par          └─────┘              
pid          └───┘└┘              
st   ───────┘└───────────────────────┘
104            by { rw ← s_dim, exact (findim_eq_card_basis b_basis).symm },
id                       └───┘         └──────────────────┘ └─────┘
src                 └───┘       └────┘ └──────────────────┘       └─────┘
typ                 └───┘└───┘  └────┘ └──────────────────┘└─────┘└─────┘
doc                 └───┘       └────┘ └──────────────────┘       └─────┘
txt                 └───┘       └────┘                            └─────┘
par                 └───┘       └────┘                            └─────┘
pid                   └─┘                                        └───┘└┘
st                └─────────┘└──────────────────────────────────────────┘└┘
105          have : continuous (equiv_fun_basis b_basis) := IH (subtype.val : b → s) this b_basis,
id                  └────────┘  └─────────────┘ └─────┘     └┘  └─────────┘        └──┘ └─────┘
src          └─────┘└────────┘ └─────────────┘       └───┘   └─────────┘└─┘   └┘    
typ          └─────┘└────────┘ └─────────────┘└─────┘└───┘└┘ └─────────┘└─┘ └┘└──┘└─────┘
doc          └─────┘└────────┘ └─────────────┘       └───┘              └─┘   └┘    
txt          └─────┘                                 └───┘              └─┘   └┘    
par          └─────┘                                 └───┘              └─┘   └┘    
pid          └───┘└┘                                 └──┘              └─┘   └┘    
st   ──────────────┘└────────┘└─────────────────────────────────────────────────────────────────┘└─
106          exact (equiv_fun_basis b_basis).symm.uniform_embedding (linear_map.continuous_on_pi _) this },
id                  └─────────────┘ └─────┘                          └─────────────────────────┘    └──┘
src          └────┘ └─────────────┘       └───────────────────────┘ └─────────────────────────┘└──┘    
typ          └────┘ └─────────────┘└─────┘└───────────────────────┘ └─────────────────────────┘└──┘└──┘
doc          └────┘ └─────────────┘       └───────────────────────┘ └─────────────────────────┘└──┘    
txt          └────┘                       └───────────────────────┘                            └──┘    
par          └────┘                       └───────────────────────┘                            └──┘    
pid                                      └───────────────────────┘                            └──┘    
st   ───────────────────────────────────────────────────────────────────────────────────────────────────┘└┘
107        have : is_complete (range ((equiv_fun_basis b_basis).symm)),
id                └─────────┘  └───┘   └─────────────┘ └─────┘
src        └─────┘└─────────┘ └───┘  └─────────────┘       └──────┘
typ        └─────┘└─────────┘ └───┘  └─────────────┘└─────┘└──────┘
doc        └─────┘└─────────┘ └───┘  └─────────────┘       └──────┘
txt        └─────┘                                         └──────┘
par        └─────┘                                         └──────┘
pid        └───┘└┘                                         └──────┘
st   ────────────────────────────────────────────────────────────────┘└─
108        { rw [← image_univ, is_complete_image_iff U],
id                 └────────┘  └───────────────────┘ 
src          └────┘└────────┘└┘└───────────────────┘ 
typ          └────┘└────────┘└┘└───────────────────┘
doc          └────┘          └┘└───────────────────┘ 
txt          └────┘          └┘                      
par          └────┘          └┘                      
pid            └──┘          └┘                      
st   ───────┘└──────────────┘└───────────────────────┘└──
109          convert complete_univ,
id                   └───────────┘
src          └──────┘└───────────┘
typ          └──────┘└───────────┘
doc          └──────┘
txt          └──────┘
par          └──────┘
pid                 
st   ────────────────────────────┘└─
110          change complete_space (b → 𝕜),
id                  └────────────┘     
src          └─────┘└────────────┘    
typ          └─────┘└────────────┘  
doc          └─────┘└────────────┘    
txt          └─────┘                  
par          └─────┘                  
pid                                  
st   ────────────────────────────────────┘
111          apply_instance },
st                          └┘
112        have : is_complete (range (subtype.val : s → E)),
id                                                      
typ                                                     
113        { change is_complete (range ((equiv_fun_basis b_basis).symm.to_equiv)) at this,
114          rw equiv.range_eq_univ at this,
115          rwa [← image_univ, is_complete_image_iff],
116          exact isometry_subtype_val.uniform_embedding },
st                                                        └┘
117        apply is_closed_of_is_complete,
118        rwa subtype.val_range at this },
st                                       └┘
119      -- second step: any linear form is continuous, as its kernel is closed by the first step
120      have H₂ : ∀f : E →ₗ[𝕜] 𝕜, continuous f,
id                             
typ                            
121      { assume f,
122        have : findim 𝕜 f.ker = n ∨ findim 𝕜 f.ker = n.succ,
id                                                     └────┘
src                                                     └────┘
typ                                                    └────┘
123        { have Z := f.findim_range_add_findim_ker,
124          rw [findim_eq_card_basis hξ, hn] at Z,
125          have : findim 𝕜 f.range = 0 ∨ findim 𝕜 f.range = 1,
id                                                
typ                                               
126          { have I : ∀(k : ℕ), k ≤ 1 ↔ k = 0 ∨ k = 1, by omega manual,
127            have : findim 𝕜 f.range ≤ findim 𝕜 𝕜 := submodule.findim_le _,
id                                                
typ                                               
128            rwa [findim_of_field, I] at this },
st                                              └┘
129          cases this,
130          { rw this at Z,
131            right,
132            simpa using Z },
st                           └┘
133          { left,
134            rw [this, add_comm, nat.add_one] at Z,
135            exact nat.succ_inj Z } },
st                                  └──┘
136        have : is_closed (f.ker : set E),
id                                   └─┘ 
src                                  └─┘
typ                                  └─┘ 
137        { cases this,
138          { exact H₁ _ this },
st                             └┘
139          { have : f.ker = ⊤,
140              by { apply eq_top_of_findim_eq, rw [findim_eq_card_basis hξ, hn, this] },
st                                                                                     └┘
141            simp [this] } },
st                         └──┘
142        exact linear_map.continuous_iff_is_closed_ker.2 this },
st                                                              └┘
143      -- third step: applying the continuity to the linear form corresponding to a coefficient in the
144      -- basis decomposition, deduce that all such coefficients are controlled in terms of the norm
145      have : ∀i:ι, ∃C, 0 ≤ C ∧ ∀(x:E), ∥equiv_fun_basis hξ x i∥ ≤ C * ∥x∥,
id                                  
typ                                 
146      { assume i,
147        let f : E →ₗ[𝕜] 𝕜 := (linear_map.proj i).comp (equiv_fun_basis hξ),
id                                             
typ                                            
148        let f' : E →L[𝕜] 𝕜 := { cont := H₂ f, ..f },
id                         
typ                        
149        exact ⟨∥f'∥, norm_nonneg _, λx, continuous_linear_map.le_op_norm f' x⟩ },
id                                      
typ                                     
st                                                                                └┘
150      -- fourth step: combine the bound on each coefficient to get a global bound and the continuity
151      choose C0 hC0 using this,
152      let C := finset.sum finset.univ C0,
id                                       └┘
typ                                      └┘
153      have C_nonneg : 0 ≤ C := finset.sum_nonneg (λi hi, (hC0 i).1),
id                                                   
typ                                                  
154      have C0_le : ∀i, C0 i ≤ C :=
id                       └┘     
typ                      └┘     
155        λi, finset.single_le_sum (λj hj, (hC0 j).1) (finset.mem_univ _),
id                                   
typ                                  
156      apply linear_map.continuous_of_bound _ C (λx, _),
id                                                 
typ                                                
157      rw pi_norm_le_iff,
158      { exact λi, le_trans ((hC0 i).2 x) (mul_le_mul_of_nonneg_right (C0_le i) (norm_nonneg _)) },
id                                      
typ                                     
st                                                                                                 └┘
159      { exact mul_nonneg C_nonneg (norm_nonneg _) } }
st                                                   └───
160  end
st   ──┘
161  
162  /-- Any linear map on a finite dimensional space over a complete field is continuous. -/
163  theorem linear_map.continuous_of_finite_dimensional [finite_dimensional 𝕜 E] (f : E →ₗ[𝕜] F') :
id                                                                                         └┘
typ                                                                                        └┘
164    continuous f :=
165  begin
166    -- for the proof, go to a model vector space `b → 𝕜` thanks to `continuous_equiv_fun_basis`, and
167    -- argue that all linear maps there are continuous.
168    rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
id                                    
typ                                   
169    letI : fintype b := finite.fintype b_finite,
id            └─────┘                    └──────┘
src           └─────┘
typ           └─────┘                    └──────┘
doc           └─────┘
170    have A : continuous (equiv_fun_basis b_basis) :=
171      continuous_equiv_fun_basis _ rfl b_basis,
172    have B : continuous (f.comp ((equiv_fun_basis b_basis).symm : (b → 𝕜) →ₗ[𝕜] E)) :=
id                                                                                
typ                                                                               
173      linear_map.continuous_on_pi _,
174    have : continuous ((f.comp ((equiv_fun_basis b_basis).symm : (b → 𝕜) →ₗ[𝕜] E))
id                                                                               
typ                                                                              
175                        ∘ (equiv_fun_basis b_basis)) := B.comp A,
176    convert this,
177    ext x,
178    simp only [linear_equiv.coe_apply, function.comp_app, coe_fn_coe_base, linear_map.comp_apply],
179    rw linear_equiv.symm_apply_apply
180  end
st   └─┘
181  
182  /-- The continuous linear map induced by a linear map on a finite dimensional space -/
183  def linear_map.to_continuous_linear_map [finite_dimensional 𝕜 E] (f : E →ₗ[𝕜] F') : E →L[𝕜] F' :=
id                                                                             └┘          └┘
typ                                                                            └┘          └┘
184  { cont := f.continuous_of_finite_dimensional, ..f }
185  
186  /-- The continuous linear equivalence induced by a linear equivalence on a finite dimensional space. -/
187  def linear_equiv.to_continuous_linear_equiv [finite_dimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : E ≃L[𝕜] F :=
id                                                                                           
typ                                                                                          
188  { continuous_to_fun := e.to_linear_map.continuous_of_finite_dimensional,
id                            └───────────┘└───────────────────────────────┘
src                           └───────────┘└───────────────────────────────┘
typ                           └───────────┘└───────────────────────────────┘
doc                                        └───────────────────────────────┘
189    continuous_inv_fun := begin
st                           └─────
190      haveI : finite_dimensional 𝕜 F := e.finite_dimensional,
id               └────────────────┘      └──────────────────┘
src      └──────┘└────────────────┘  └──┘└──────────────────┘
typ      └──────┘└────────────────┘└──┘└──────────────────┘
doc      └──────┘└────────────────┘  └──┘└──────────────────┘
txt      └──────┘                    └──┘
par      └──────┘                    └──┘
pid           └┘                    └──┘
st   ─────────────────────────────────────────────────────────┘└─
191      exact e.symm.to_linear_map.continuous_of_finite_dimensional
id             └───────────────────────────────────────────────────┘
src      └────┘└───────────────────────────────────────────────────┘
typ      └────┘└───────────────────────────────────────────────────┘
doc      └────┘└───────────────────────────────────────────────────┘
txt      └────┘                                                     
par      └────┘                                                     
pid                                                                
st   ────────────────────────────────────────────────────────────────
192    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
193    ..e }
id       
typ      
194  
195  /-- Any finite-dimensional vector space over a complete field is complete.
196  We do not register this as an instance to avoid an instance loop when trying to prove the
197  completeness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance
198  explicitly when needed. -/
199  variables (𝕜 E)
200  lemma finite_dimensional.complete [finite_dimensional 𝕜 E] : complete_space E :=
id                                      └────────────────┘      └────────────┘ 
src                                     └────────────────┘        └────────────┘
typ                                     └────────────────┘      └────────────┘ 
doc                                     └────────────────┘        └────────────┘
201  begin
st   └─────
202    rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
id            └────────────────────┘  
src    └─────┘└────────────────────┘  └──────────────────────────┘
typ    └─────┘└────────────────────┘└──────────────────────────┘
doc    └─────┘                        └──────────────────────────┘
txt    └─────┘                        └──────────────────────────┘
par    └─────┘                        └──────────────────────────┘
pid                                  └──────────────────────────┘
st   ──────────────────────────────────────────────────────────────┘└─
203    letI : fintype b := finite.fintype b_finite,
id            └─────┘     └────────────┘ └──────┘
src    └─────┘└─────┘ └──┘└────────────┘
typ    └─────┘└─────┘└──┘└────────────┘└──────┘
doc    └─────┘└─────┘ └──┘└────────────┘
txt    └─────┘        └──┘              
par    └─────┘        └──┘              
pid        └┘        └──┘              
st   ────────────────────────────────────────────┘└─
204    have : uniform_embedding (equiv_fun_basis b_basis).symm :=
id            └───────────────┘  └─────────────┘ └─────┘
src    └─────┘└───────────────┘ └─────────────┘       └─────────
typ    └─────┘└───────────────┘ └─────────────┘└─────┘└─────────
doc    └─────┘                  └─────────────┘       └─────────
txt    └─────┘                                        └─────────
par    └─────┘                                        └─────────
pid    └───┘└┘                                        └───┘└────
st   ─────────────────────────────────────────────────────────────
205      linear_equiv.uniform_embedding _ (linear_map.continuous_of_finite_dimensional _)
id       └────────────────────────────┘
src  ───┘└────────────────────────────┘└─┘                                            └───
typ  ───┘└────────────────────────────┘└─┘                                            └───
doc  ───┘└────────────────────────────┘└─┘                                            └───
txt  ───┘                              └─┘                                            └───
par  ───┘                              └─┘                                            └───
pid  ───┘                              └─┘                                            └───
st   ─────────────────────────────────────────────────────────────────────────────────────
206      (linear_map.continuous_of_finite_dimensional _),
id        └─────────────────────────────────────────┘
src  ───┘ └─────────────────────────────────────────┘└─┘
typ  ───┘ └─────────────────────────────────────────┘└─┘
doc  ───┘ └─────────────────────────────────────────┘└─┘
txt  ───┘                                            └─┘
par  ───┘                                            └─┘
pid  ───┘                                            └─┘
st   ──────────────────────────────────────────────────┘└─
207    have : is_complete ((equiv_fun_basis b_basis).symm.to_equiv '' univ) :=
id            └─────────┘   └─────────────┘ └─────┘                └┘ └──┘
src    └─────┘└─────────┘  └─────────────┘       └──────────────┘└┘└──┘└────
typ    └─────┘└─────────┘  └─────────────┘└─────┘└──────────────┘└┘└──┘└────
doc    └─────┘└─────────┘  └─────────────┘       └──────────────┘      └────
txt    └─────┘                                   └──────────────┘      └────
par    └─────┘                                   └──────────────┘      └────
pid    └───┘└┘                                   └──────────────┘      └───
st   ──────────────────────────────────────────────────────────────────────────
208      (is_complete_image_iff this).mpr complete_univ,
id        └───────────────────┘           └───────────┘
src  ───┘ └───────────────────┘    └────┘└───────────┘
typ  ───┘ └───────────────────┘    └────┘└───────────┘
doc  ───┘ └───────────────────┘    └────┘
txt  ───┘                          └────┘
par  ───┘                          └────┘
pid  ───┘                          └────┘
st   ──────────────────────────┘    └─────────────────┘
209    rw [image_univ, equiv.range_eq_univ] at this,
210    exact complete_space_of_is_complete_univ this
211  end
st   └─┘
212  
213  variables {𝕜 E}
214  /-- A finite-dimensional subspace is complete. -/
215  lemma submodule.complete_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
id                                                       └───────┘     └────────────────┘  
src                                                      └───────┘       └────────────────┘
typ                                                      └───────┘     └────────────────┘  
doc                                                      └───────┘       └────────────────┘
216    is_complete (s : set E) :=
id     └─────────┘     └─┘ 
src    └─────────┘      └─┘
typ    └─────────┘     └─┘ 
doc    └─────────┘
217  begin
st   └─────
218    haveI : complete_space s := finite_dimensional.complete 𝕜 s,
id             └────────────┘     └─────────────────────────┘  
src    └──────┘└────────────┘ └──┘└─────────────────────────┘ 
typ    └──────┘└────────────┘└──┘└─────────────────────────┘
doc    └──────┘└────────────┘ └──┘                            
txt    └──────┘               └──┘                            
par    └──────┘               └──┘                            
pid         └┘               └──┘                            
st   ────────────────────────────────────────────────────────────┘└─
219    have : is_complete (range (subtype.val : s → E)),
id            └─────────┘  └───┘  └─────────┘      
src    └─────┘└─────────┘ └───┘ └─────────┘└─┘   └┘
typ    └─────┘└─────────┘ └───┘ └─────────┘└─┘ └┘
doc    └─────┘└─────────┘ └───┘            └─┘   └┘
txt    └─────┘                             └─┘   └┘
par    └─────┘                             └─┘   └┘
pid    └───┘└┘                             └─┘   └┘
st   ─────────────────────────────────────────────────┘└─
220    { rw [← image_univ, is_complete_image_iff],
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid        └──┘
st   ───┘└──────────────┘
221      { exact complete_univ },
st                             
222      { exact isometry_subtype_val.uniform_embedding } },
st                                                      └─┘
223    rwa subtype.val_range at this
224  end
st   └─┘
225  
226  /-- A finite-dimensional subspace is closed. -/
227  lemma submodule.closed_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
id                                                     └───────┘     └────────────────┘  
src                                                    └───────┘       └────────────────┘
typ                                                    └───────┘     └────────────────┘  
doc                                                    └───────┘       └────────────────┘
228    is_closed (s : set E) :=
id     └───────┘     └─┘ 
src    └───────┘      └─┘
typ    └───────┘     └─┘ 
doc    └───────┘
229  is_closed_of_is_complete s.complete_of_finite_dimensional
id   └──────────────────────┘ 
src  └──────────────────────┘  
typ  └──────────────────────┘ 
doc                            
230  
231  end complete_field
232  
233  section proper_field
234  variables (𝕜 : Type u) [nondiscrete_normed_field 𝕜]
id                           └──────────────────────┘
src                          └──────────────────────┘
typ                          └──────────────────────┘
doc                          └──────────────────────┘
235  (E : Type v) [normed_group E] [normed_space 𝕜 E] [proper_space 𝕜]
id                 └──────────┘     └──────────┘       └──────────┘
src                └──────────┘     └──────────┘       └──────────┘
typ                └──────────┘     └──────────┘       └──────────┘
doc                └──────────┘     └──────────┘       └──────────┘
236  
237  /-- Any finite-dimensional vector space over a proper field is proper.
238  We do not register this as an instance to avoid an instance loop when trying to prove the
239  properness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance
240  explicitly when needed. -/
241  lemma finite_dimensional.proper [finite_dimensional 𝕜 E] : proper_space E :=
id                                    └────────────────┘      └──────────┘ 
src                                   └────────────────┘        └──────────┘
typ                                   └────────────────┘      └──────────┘ 
doc                                   └────────────────┘        └──────────┘
242  begin
st   └─────
243    rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
id            └────────────────────┘  
src    └─────┘└────────────────────┘  └──────────────────────────┘
typ    └─────┘└────────────────────┘└──────────────────────────┘
doc    └─────┘                        └──────────────────────────┘
txt    └─────┘                        └──────────────────────────┘
par    └─────┘                        └──────────────────────────┘
pid                                  └──────────────────────────┘
st   ──────────────────────────────────────────────────────────────┘└─
244    letI : fintype b := finite.fintype b_finite,
id            └─────┘     └────────────┘ └──────┘
src    └─────┘└─────┘ └──┘└────────────┘
typ    └─────┘└─────┘└──┘└────────────┘└──────┘
doc    └─────┘└─────┘ └──┘└────────────┘
txt    └─────┘        └──┘              
par    └─────┘        └──┘              
pid        └┘        └──┘              
st   ────────────────────────────────────────────┘└─
245    let e := equiv_fun_basis b_basis,
id              └─────────────┘ └─────┘
src    └───────┘└─────────────┘
typ    └───────┘└─────────────┘└─────┘
doc    └───────┘└─────────────┘
txt    └───────┘               
par    └───────┘               
pid    └───┘└─┘               
st   ─────────────────────────────────┘
246    let f : E →L[𝕜] (b → 𝕜) :=
id                         
typ                        
247      { cont := linear_map.continuous_of_finite_dimensional _, ..e.to_linear_map },
248    refine metric.proper_image_of_proper e.symm
249      (linear_map.continuous_of_finite_dimensional _) _ (∥f∥)  (λx y, _),
250    { exact equiv.range_eq_univ e.symm.to_equiv },
st                                                 └┘
251    { have A : e (e.symm x) = x := linear_equiv.apply_symm_apply _ _,
252      have B : e (e.symm y) = y := linear_equiv.apply_symm_apply _ _,
253      conv_lhs { rw [← A, ← B] },
254      change dist (f (e.symm x)) (f (e.symm y)) ≤ ∥f∥ * dist (e.symm x) (e.symm y),
255      exact f.lipschitz _ _ }
st                             └─
256  end
st   ──┘
257  
258  end proper_field
259  
260  /- Over the real numbers, we can register the previous statement as an instance as it will not
261  cause problems in instance resolution since the properness of `ℝ` is already known. -/
262  instance finite_dimensional.proper_real
263    (E : Type u) [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] : proper_space E :=
id                   └┘  └──┘  └┘                                                          
src                  └┘  └──┘  └┘                                          
typ                  └┘  └──┘  └┘                                                          
doc                  └┘  └──┘  └┘
264  finite_dimensional.proper ℝ E
id                              
src                            
typ                             
265  
266  attribute [instance, priority 900] finite_dimensional.proper_real